a:. prime(a)  Prop 

latex

Definitions	prime(a), P & Q, A, a ~ b, P  Q, P  Q, Prop, b | a, x:A. B(x), t  T
Lemmas	divides wf, assoced wf, not wf